﻿using System.Collections.Generic;
using Microsoft.ExtendedReflection.Collections;
using Microsoft.ExtendedReflection.ComponentModel;
using Microsoft.ExtendedReflection.Interpretation;
using Microsoft.ExtendedReflection.Interpretation.Visitors;
using Microsoft.ExtendedReflection.Metadata;
using Microsoft.ExtendedReflection.Reasoning;
using Microsoft.ExtendedReflection.Utilities;
using Microsoft.ExtendedReflection.Utilities.Safe.Diagnostics;
using Microsoft.ExtendedReflection.Utilities.Safe.IO;
using Microsoft.Pex.Engine.ComponentModel;
using Microsoft.Pex.Engine.Drivers;
using Microsoft.Pex.Engine.PostAnalysis;
using Microsoft.Pex.Framework.Packages;

namespace SatisfiableChecker
{
    public sealed class SatisfiableCheckerAttribute
        : PexPathPackageAttributeBase
    {
        protected override object BeforeRun(IPexPathComponent host)
        {
            return null;
        }

        protected override void AfterRun(IPexPathComponent host, object data)
        {
            host.Log.LogMessage("Satisfiable Checker", "begin");

            var controller = new SatisfiableTrackingController();
            Term[] conditionsToCheck;
            using (IEngine trackingEngine = host.PathServices.TrackingEngineFactory.CreateTrackingEngine(controller))
            {
                trackingEngine.GetService<IPexTrackingDriver>().Run();
                conditionsToCheck = controller.ConditionsToCheck;
            }            

            var termManager = host.ExplorationServices.TermManager;
            var solverFactory = host.ExplorationServices.SolverFactory;
            var solverStatistics = solverFactory.CreateStatistics();
            foreach (var condition in conditionsToCheck)
            {
                var variables = VariablesCollector.Collect(termManager, condition);
                using (var solver = solverFactory.CreateSolver(solverStatistics))
                {
                    var writer = new SafeStringWriter();
                    foreach (var symbolIdWithType in variables)
                    {
                        writer.WriteLine("variable: {0}", symbolIdWithType.Description);
                        solver.AddDomainVariable(0, symbolIdWithType);
                    }
                    writer.WriteLine("condition: {0}", prettyPrintTerm(host, condition, SystemTypes.Bool));

                    solver.Assert("is satisfiable check", condition);
                    IModel model;
                    var result = solver.TryGetModel(null, out model);
                    writer.WriteLine(" MyTryGetModel => {0}", result);
                    if (result == TryGetModelResult.Success)
                        foreach (var symbolIdWithType in variables)
                        {
                            writer.Write("{0} => ", symbolIdWithType.Description);
                            var variable = termManager.Symbol(symbolIdWithType);
                            var value = model.GetValue(variable);
                            writer.WriteLine(prettyPrintTerm(host, value, symbolIdWithType.Type));

                            TypeEx type;

                            if (symbolIdWithType.Layout.Kind == LayoutKind.Ref &&
                                termManager.TryGetObjectType(value, out type) &&
                                type != SystemTypes.Null)
                            {
                                foreach (var field in type.InstanceFields)
                                {
                                    var fieldVariable = termManager.SelectInstanceFieldInInitialState(variable, field);
                                    var fieldValue = model.GetValue(fieldVariable);

                                    writer.Write("{0}.{1} => ", symbolIdWithType.Description, field.ShortName);
                                    writer.WriteLine(prettyPrintTerm(host, fieldValue, field.Type));

                                    TypeEx fieldValueType;
                                    if (termManager.TryGetObjectType(fieldValue, out fieldValueType)) // is this an object, and if so, what’s its type?
                                    {
                                        // do the same thing are before for the nested fields
                                        foreach (var nestedField in field.Type.InstanceFields)
                                        {
                                            var nestedFieldVariable = termManager.SelectInstanceFieldInInitialState(fieldValue, nestedField);
                                            var nestedFieldValue = model.GetValue(nestedFieldVariable);
                                            writer.Write("{0}.{1}.{2} => ", symbolIdWithType.Description, field.ShortName, nestedField.ShortName);
                                            writer.WriteLine(prettyPrintTerm(host, nestedFieldValue, nestedField.Type));
                                        }
                                    }
                                }
                            }
                        }
                    if (model != null) model.Dispose();

                    host.Log.Dump("Satisfiable Checker", "check", writer.ToString());
                }
            }

            host.Log.LogMessage("Satisfiable Checker", "end");
        }

        private static string prettyPrintTerm(IPexPathComponent host, Term term, TypeEx type)
        {
            var writer = new SafeStringWriter();
            var codeWriter = host.Services.TestManager.Language.CreateBodyWriter(
                writer,
                VisibilityContext.Private,
                100);
            var emitter = new TermEmitter(
                 host.ExplorationServices.TermManager,
                 new NameCreator());

            if (!emitter.TryEvaluate(
                    new Term[] { term },
                    10000, // bound on size of expression we are going to pretty-print
                    codeWriter))
            {
                writer.WriteLine("(expression too big; consider using environment variable {0})", ExtendedReflectionEnvironmentSettings.NoCodeEmitterSizeLimit.Name);
            }
            else
            {
                codeWriter.Return(type);
            }
            return writer.ToString();
        }

        sealed class VariablesCollector : TermInternalizingRewriter<TVoid>
        {
            SafeSet<ISymbolIdWithType> variables = new SafeSet<ISymbolIdWithType>();
            VariablesCollector(TermManager termManager) : base(termManager, OnCollection.Fail) { }
            public override Term VisitSymbol(TVoid parameter, Term term, ISymbolId key)
            {
                if (key is ISymbolIdWithType)
                    this.variables.Add((ISymbolIdWithType)key);
                return term;
            }
            public static ISymbolIdWithType[] Collect(TermManager termManager, Term term)
            {
                using (var collector = new VariablesCollector(termManager))
                {
                    collector.VisitTerm(default(TVoid), term);
                    return collector.variables.ToArray();
                }
            }
        }

        sealed class SatisfiableTrackingController
            : PexTrackingControllerBase
        {
            /// <summary>
            /// frame id that will be associated with all top-level methods, i.e. object factories and PUTs
            /// </summary>
            const int TopLevelMethodFrameId = 1;
            /// <summary>
            /// frame id that will be associated with all non-top-level methods
            /// </summary>
            const int OtherMethodFrameId = 0;

            static TypeEx satisfiableHelperType = MetadataFromReflection.GetType(typeof(SatisfiableHelper));
            static Method satisfiableCheckMethod = satisfiableHelperType.GetMethod("Check", SystemTypes.Bool);

            #region state
            SafeList<Term> conditionsToCheck = new SafeList<Term>();
            public Term[] ConditionsToCheck { get { return conditionsToCheck.ToArray(); } }
            #endregion

            #region Callbacks to keep track of depth of call stack, and frame ids
            int depth;
            public override int GetNextFrameId(int threadId, Microsoft.ExtendedReflection.Metadata.Method method)
            {
                return depth++ == 0 ? TopLevelMethodFrameId : OtherMethodFrameId;
            }
            public override void FrameDisposed(int frameId, PexTrackingFrame frame)
            {
                depth--;
            }
            #endregion

            #region Callbacks to inject and consume symbols for arguments
            public override PexArgumentTracking GetArgumentTreatment(PexTrackingThread thread, int frameId, Method method)
            {
                if (frameId == TopLevelMethodFrameId)
                    return PexArgumentTracking.Track;
                else
                    return PexArgumentTracking.Derived;
            }

            public override void DerivedArguments(int frameId, Method method, Term[] arguments)
            {
                if (method == satisfiableCheckMethod)
                {
                    var normalizedCondition = this.TermManager.IsNotDefault(arguments[0]);
                    SafeDebug.Assert(this.TermManager.IsProperStackBoolean(normalizedCondition), "condition has been normalized to be either 0 or 1 as a 32-bit integer");
                    var pathConditionAndLocalCondition =
                        this.TermManager.LogicalAnd(
                            this.PathConditionBuilder.Condition,
                            normalizedCondition);
                    SafeDebug.Assert(this.TermManager.IsProperStackBoolean(pathConditionAndLocalCondition), "condition has been normalized to be either 0 or 1 as a 32-bit integer");
                    conditionsToCheck.Add(pathConditionAndLocalCondition);
                }
            }
            #endregion

            #region Don't do anything special with all other callbacks
            public override void FrameHasExceptions(int frameId, Method method) { }
            public override void FrameHasExplicitFailures(int frameId, Method method, IEnumerable<object> exceptionObjects) { }
            #endregion
        }
    }
}